{
 "metadata": {
  "language_info": {
   "codemirror_mode": {
    "name": "ipython",
    "version": 3
   },
   "file_extension": ".py",
   "mimetype": "text/x-python",
   "name": "python",
   "nbconvert_exporter": "python",
   "pygments_lexer": "ipython3",
   "version": "3.7.3"
  },
  "orig_nbformat": 2,
  "kernelspec": {
   "name": "python3",
   "display_name": "Python 3.7.3 64-bit ('ml2': pyenv)"
  },
  "metadata": {
   "interpreter": {
    "hash": "6777b983a30343457facb6d641fab749a3d1ac686971770ba4e1636635b77c7f"
   }
  },
  "interpreter": {
   "hash": "8caa4319d59a734f94e739df6b594acde678ec5f2e3eb7152d087fc4a1992669"
  }
 },
 "nbformat": 4,
 "nbformat_minor": 2,
 "cells": [
  {
   "cell_type": "markdown",
   "source": [],
   "metadata": {}
  },
  {
   "cell_type": "markdown",
   "source": [
    "# LTL Synthesis Transformer Experiment"
   ],
   "metadata": {}
  },
  {
   "cell_type": "markdown",
   "source": [
    "## Imports"
   ],
   "metadata": {}
  },
  {
   "cell_type": "code",
   "execution_count": 1,
   "source": [
    "import tensorflow as tf\n",
    "\n",
    "from ml2.ltl import LTLSpec\n",
    "from ml2.ltl.ltl_syn.ltl_syn_transformer_experiment import LTLSynTransformerExperiment"
   ],
   "outputs": [],
   "metadata": {}
  },
  {
   "cell_type": "markdown",
   "source": [
    "## Create Experiment"
   ],
   "metadata": {}
  },
  {
   "cell_type": "code",
   "execution_count": null,
   "source": [
    "experiment = LTLSynTransformerExperiment()"
   ],
   "outputs": [],
   "metadata": {}
  },
  {
   "cell_type": "markdown",
   "source": [
    "## Run Experiment"
   ],
   "metadata": {}
  },
  {
   "cell_type": "code",
   "execution_count": null,
   "source": [
    "experiment.run(stream_to_wandb=True)"
   ],
   "outputs": [],
   "metadata": {
    "tags": []
   }
  },
  {
   "cell_type": "markdown",
   "source": [
    "## Load Experiment"
   ],
   "metadata": {}
  },
  {
   "cell_type": "code",
   "execution_count": 2,
   "source": [
    "experiment = LTLSynTransformerExperiment.load('transformer-1')"
   ],
   "outputs": [
    {
     "output_type": "stream",
     "name": "stderr",
     "text": [
      "INFO:ml2.artifact:Found experiment transformer-1 locally\n",
      "INFO:ml2.experiment:Initialized experiment with arguments:\n",
      "aiger_order: ['inputs', 'latches', 'outputs', 'ands']\n",
      "aiger_unfold_latches: False\n",
      "aiger_unfold_negations: False\n",
      "alpha: 0.5\n",
      "batch_size: 256\n",
      "beam_size: 1\n",
      "cache_dataset: True\n",
      "checkpoint_monitor: val_accuracy_per_sequence\n",
      "constant_learning_rate: None\n",
      "custom_pos_enc: True\n",
      "d_embed_dec: 256\n",
      "d_embed_enc: 256\n",
      "d_ff: 1024\n",
      "dataset_name: scpa-2\n",
      "drop_batch_remainder: True\n",
      "dropout: 0.0\n",
      "dtype_float: <dtype: 'float32'>\n",
      "dtype_int: <dtype: 'int32'>\n",
      "encode_realizable: True\n",
      "ff_activation: relu\n",
      "group: None\n",
      "initial_steps: 0\n",
      "inputs: ['i0', 'i1', 'i2', 'i3', 'i4']\n",
      "max_input_length: 128\n",
      "max_target_length: 128\n",
      "name: transformer-1\n",
      "num_heads: 4\n",
      "num_layers_dec: 8\n",
      "num_layers_enc: 8\n",
      "outputs: ['o0', 'o1', 'o2', 'o3', 'o4']\n",
      "parent_name: \n",
      "shuffle_on_load: False\n",
      "steps: 30000\n",
      "tf_shuffle_buffer_size: 0\n",
      "val_freq: 100\n",
      "warmup_steps: 4000\n",
      "WARNING:ml2.experiment:Experiment transformer-1 already exists locally\n"
     ]
    }
   ],
   "metadata": {}
  },
  {
   "cell_type": "markdown",
   "source": [
    "## Evaluate Test Set"
   ],
   "metadata": {
    "tags": []
   }
  },
  {
   "cell_type": "code",
   "execution_count": null,
   "source": [
    "experiment.batch_size = 16\n",
    "experiment.beam_size = 16\n",
    "experiment.alpha = 0.5"
   ],
   "outputs": [],
   "metadata": {}
  },
  {
   "cell_type": "code",
   "execution_count": null,
   "source": [
    "experiment.eval('test', steps=8, training=False, verify=True)"
   ],
   "outputs": [],
   "metadata": {
    "tags": []
   }
  },
  {
   "cell_type": "markdown",
   "source": [
    "## Evaluate SYNTCOMP"
   ],
   "metadata": {}
  },
  {
   "cell_type": "code",
   "execution_count": null,
   "source": [
    "experiment.eval_ltl_specs('sc-0')"
   ],
   "outputs": [],
   "metadata": {
    "tags": []
   }
  },
  {
   "cell_type": "markdown",
   "source": [
    "## Evaluate Timeouts"
   ],
   "metadata": {}
  },
  {
   "cell_type": "code",
   "execution_count": null,
   "source": [
    "experiment.eval_timeouts(steps=8, training=False)"
   ],
   "outputs": [],
   "metadata": {}
  },
  {
   "cell_type": "markdown",
   "source": [
    "## Evaluate Smart Home Benchmarks"
   ],
   "metadata": {}
  },
  {
   "cell_type": "code",
   "execution_count": null,
   "source": [
    "experiment.eval_bosy_files('syntcomp/tsl_smart_home_jarvis')"
   ],
   "outputs": [],
   "metadata": {}
  },
  {
   "cell_type": "markdown",
   "source": [
    "## Analyze Evaluations"
   ],
   "metadata": {}
  },
  {
   "cell_type": "code",
   "execution_count": null,
   "source": [
    "EVAL_DIR = ''\n",
    "experiment.analyze_eval_circuits(\n",
    "    EVAL_DIR,\n",
    "    buckets=[5, 10, 15, 20],\n",
    "    property='Num AND Gates',\n",
    "    title='Test Set',\n",
    "    width=3.0,\n",
    "    xlabel='Number of AND Gates')"
   ],
   "outputs": [],
   "metadata": {
    "tags": []
   }
  },
  {
   "cell_type": "code",
   "execution_count": null,
   "source": [
    "FILEPATH = ''\n",
    "experiment.analyze_eval_file_realizability(FILEPATH)\n"
   ],
   "outputs": [],
   "metadata": {}
  },
  {
   "cell_type": "markdown",
   "source": [
    "## Call Model"
   ],
   "metadata": {}
  },
  {
   "cell_type": "code",
   "execution_count": 3,
   "source": [
    "spec_dict = {\n",
    "    \"guarantees\": [\n",
    "        \"G (! o0 | ! o1)\",\n",
    "        \"(G ((i0) -> (F (o0))))\",\n",
    "        \"(G ((i1) -> (F (o1))))\"\n",
    "      ],\n",
    "      \"inputs\": [\n",
    "        \"i0\",\n",
    "        \"i1\",\n",
    "        \"i2\",\n",
    "        \"i3\",\n",
    "        \"i4\"\n",
    "      ],\n",
    "      \"outputs\": [\n",
    "        \"o0\",\n",
    "        \"o1\",\n",
    "        \"o2\",\n",
    "        \"o3\",\n",
    "        \"o4\"\n",
    "      ],\n",
    "}"
   ],
   "outputs": [],
   "metadata": {}
  },
  {
   "cell_type": "code",
   "execution_count": 4,
   "source": [
    "problem = LTLSpec.from_dict(spec_dict)"
   ],
   "outputs": [],
   "metadata": {}
  },
  {
   "cell_type": "code",
   "execution_count": null,
   "source": [
    "experiment.call(problem, training=False, verify=True)"
   ],
   "outputs": [],
   "metadata": {}
  },
  {
   "cell_type": "code",
   "execution_count": 5,
   "source": [
    "experiment.attn_weights(problem)"
   ],
   "outputs": [
    {
     "output_type": "stream",
     "name": "stderr",
     "text": [
      "INFO:root:Constructed vocabulary containing 22 tokens\n",
      "INFO:ml2.seq2seq_experiment:Initialized input encoder\n",
      "2021-09-17 10:52:41.699736: I tensorflow/core/platform/cpu_feature_guard.cc:142] This TensorFlow binary is optimized with oneAPI Deep Neural Network Library (oneDNN) to use the following CPU instructions in performance-critical operations:  AVX2 FMA\n",
      "To enable them in other operations, rebuild TensorFlow with the appropriate compiler flags.\n",
      "INFO:root:Constructed vocabulary containing 68 tokens\n",
      "INFO:ml2.seq2seq_experiment:Initialized target encoder\n"
     ]
    },
    {
     "output_type": "stream",
     "name": "stdout",
     "text": [
      "Tensor(\"transformer/strided_slice_22:0\", shape=(), dtype=int32)\n",
      "Tensor(\"transformer/strided_slice_23:0\", shape=(), dtype=int32)\n"
     ]
    },
    {
     "output_type": "stream",
     "name": "stderr",
     "text": [
      "INFO:ml2.ltl.ltl_syn.ltl_syn_transformer_experiment:Created attention model\n",
      "INFO:ml2.ltl.ltl_syn.ltl_syn_transformer_experiment:Found checkpoint /Users/Frederik/ml2-storage/ltl-syn/transformer-1/checkpoint\n",
      "INFO:ml2.ltl.ltl_syn.ltl_syn_transformer_experiment:Loaded weights from checkpoint\n"
     ]
    },
    {
     "output_type": "stream",
     "name": "stdout",
     "text": [
      "tf.Tensor(1, shape=(), dtype=int32)\n",
      "tf.Tensor(1, shape=(), dtype=int32)\n"
     ]
    },
    {
     "output_type": "execute_result",
     "data": {
      "text/plain": [
       "[{'circuit': 'aag 6 5 1 5 0\\n2\\n4\\n6\\n8\\n10\\n12 13\\n13\\n12\\n0\\n0\\n0\\ni0 i0\\ni1 i1\\ni2 i2\\ni3 i3\\ni4 i4\\nl0 l0\\no0 o0\\no1 o1\\no2 o2\\no3 o3\\no4 o4'}]"
      ]
     },
     "metadata": {},
     "execution_count": 5
    }
   ],
   "metadata": {}
  }
 ]
}